| Definitions | t  T, M.(timed)state, if b then t else f fi , (i = j),  x.A(x), M.init(x)?v, M(i), t.1, f(a), CV(F), d-comp(D; v; sched; dec; d), n - m, #$n,  , A  B,  A, False, P   Q, a < b,  , M.state, b dom(M.prob), Outcome, ma-prob(M;b), Void, IdLnk, Type, Unit, hd(l),  x:A. B(x),  , {x:A| B(x)} , Atom$n, Feasible(D), Dsys, x:A  B(x),  x:A. B(x), P  Q, left + right, P & Q, A c B, Msg(M), M.dout(l,tg), i  j , Id,  b, d-world-state(D;i), d-decl(D;i), Knd, s = t, x:A  B(x), {i..j }, P  Q,  b,  , timedState(ds), n+m, -n, suptype(S; T), i j < k, S  T, let x = a in b(x), World, d-partial-world(D;f;t';s;d), P Q,  T, p q, i = j, destination(l), i <z j, ||as||, Msg, queue(l;t), p q, i z j, True, doact(k;v), rcv(l,tg), mtag(m), w.M, mval(m), w-action-dec(TA;M;i), locl(a), kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), {T}, a = b, mlnk(m), MsgA, <a, b>, source(l), stutter-state(s), shift-state(s), next-world-state(D;i;s;k;v), isrcv(k), type List, msg(l;t;v), d-world(D;v;sched;dec;discrete), d-comp-partial-world(D; v; sched; dec; discrete; t), M.dout2(l;tg), SQType(T), s ~ t, State(ds), Feasible(M), finite-type(T), M.ds(x),  , Dec(P), rcvs(l;t), snds(l;t), case b of inl(x) => s(x) | inr(y) => t(y), read-state(s), M.ef(k,x,s,v)?w, M.da(a), M.din(l,tg), M.Msg, M.sends(k,s,v), null, w-knum(w;i;k;t), ma-prob-da(M), ma-prob-da-dom(M;b), inr x , isrcv_locl{isrcv_locl_compseq_tag_def:ObjectId}(a), f(x)?z |
| Lemmas | ma-da wf, locl wf, w-knum wf, subtype rel list, ma-send-val wf, mlnk wf d, ma-msg wf, filter type, doact wf, d-decl-subtype, ma-ef-val wf, read-state wf, shift-state wf, false wf, subtype rel self, Knd sq, mtag wf, decidable int equal, d-comp-partial-world wf, ma-dout2 wf, w-queue-partial, mval wf, islocal wf, tagof wf, lnk wf, msg wf, d-world wf, Msg wf, ge wf, isrcv wf, next-world-state wf, d-decl wf, stutter-state wf, lsrc wf, msga wf, ma-dout wf, mlnk-hd-w-queue, eq id wf, assert-eq-id, assert-d-eq-Loc, rcv one one, not rcv locl, Knd wf, rcv wf, hd wf, le int wf, bor wf, w-queue wf, w-Msg wf, length wf1, lt int wf, ldst wf, d-eq-Loc wf, band wf, assert of le int, or functionality wrt iff, assert of bor, bnot of lt int, bnot thru band, true wf, squash wf, assert of lt int, and functionality wrt iff, assert of band, world wf, d-partial-world wf, le wf, CV wf, ma-init-val wf, assert wf, not wf, bnot wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, d-world-state wf, int seg wf, d-comp wf2, nat properties, dsys wf, unit wf, IdLnk wf, nat wf, Id wf, d-m wf, ma-tst wf, ma-prob wf, p-outcome wf, ma-prob-dom wf, ifthenelse wf, ma-st wf, bool wf, d-feasible wf |
dec:(i,a:Id